$\forall$$A$, $B$:Type, $f$:($A$$\rightarrow$$B$), $x$:$A$, $a$:Atom1.
\\[0ex]AtomFree(Type;$A$) $\Rightarrow$ AtomFree(Type;$B$) $\Rightarrow$ $f$($x$):$B$$>>$$a$ $\Rightarrow$ $f$:$A$$\rightarrow$$B$$>>$$a$ $\vee$ $x$:$A$$>>$$a$